| Model: | nand v.1 (DTMC) |
| Parameter(s) | N = 60, K = 4 |
| Property: | reliable (prob-reach) |
~/storm/build/bin/storm --prism nand.prism --prop nand.props reliable --constants N=60,K=4 --exact floats --general:precision 1e-20 --ddlib sylvan --sylvan:maxmem 6114 --sylvan:threads 4
| Walltime: | 89.49804878234863s |
| Return code: | 0 |
| Note(s): | The tool result '686721458919267724319013/1000000000000000000000000' is tagged as incorrect. The reference result is '674375412048286579998391053568044024839796891188436079164933195932504006859863176668618453626567200815744325954013096026732016576292941767289283443813273798927471369808814227780678597502526283170376011143732046040738638479975488052191318262796730887423499092060055764460808570555973414684635167757065338750791739331293858988603042989487945582955712491974590260039905065741873854885714298872588020623965467400282885463166739143535812717697199273310102277971278786945528949661789220074183715013841242260836804042248270660085557976363578175644872898551287821380993759020250450057165990145439180550980345336796910958837967490732422873158833390335926967641639016077401593504779192627736207826140866888177394711176343476439862638983111578860864406915339169201668448685867985486117826497430887145901618112836384648567977530826248389205029495657410593836586948449805252838334427173444580925770987996143922689432502457408017259242081442839253964797127083172809304607437564123586401108004199299044292446541/982021754656721722716655706411222385507669639910781715967345406263201783692889897878427213212990938612763788231403389744767067663614743521859183275654310118412922964549494284527781431535499684177432434122301448144083942764451247133599577036672904647064298810598161393171352158933989819282448394583468262131119361851408297476380158691952302398288740119725979550137284712658047394731931729250052156222114008241553695693345821266964444821100463081039235040824849892155915658833109729829406529861748248993399079598686019016345103724868380607355278949134904844556514833763239300674164534870820578969104145515316399053092033353590698921512459580587666964268557149107720604442375672662685956383159528500472087293439870951895677831469622118461029958936824764580705546202761417280408696752629675501504845173358369477857440457221826064912064573000278911442195364772677516118775811496516055643960074429058958872529316863619897048920392990112304687500000000000000000000000000000000000000000000000000000000000' (approx. 0.6867214589192305) which means a relative error of '5.4205061836599116e-14' which is larger than the goal precision '1e-14'. |
| Relative Error: | 5.4205061836599116e-14 |
Storm 1.5.1 Date: Tue Apr 28 13:09:03 2020 Command line arguments: --prism nand.prism --prop nand.props reliable --constants 'N=60,K=4' --exact floats '--general:precision' 1e-20 --ddlib sylvan '--sylvan:maxmem' 6114 '--sylvan:threads' 4 Current working directory: / WARN (GeneralSettings.cpp:110): Setting the precision option with module prefix does not effect all solvers. Consider setting --precision instead of --general:precision. Time for model input parsing: 0.021s. Time for model construction: 70.766s. -------------------------------------------------------------- Model type: DTMC (sparse) States: 18826082 Transitions: 29772212 Reward Models: none State Labels: 3 labels * deadlock -> 0 item(s) * ((s = 4) & ((z / 60) < 1/10)) -> 6 item(s) * init -> 1 item(s) Choice Labels: none -------------------------------------------------------------- Model checking property "reliable": P=? [F ((s = 4) & ((z / 60) < 1/10))] ... Result (for initial states): 0.686721458919267724319013 Time for model checking: 18.431s.